i, j:. (i * j)   

latex

Up	int 2, int 2
Definitions	t  T, , x:A. B(x), i  j , False, A, A  B, P  Q,
Lemmas	nat wf, le wf, ge wf, nat properties